The present invention is in the general field of exploring the behavior of a design and in particular hardware design of a semiconductor chip.
[1] xe2x80x9cFormal Methods in System Designxe2x80x94An International Journalxe2x80x9d Edmund Clarke (Ed.) Kluwer Academic Publishing 1985-present.
[2] Sequential Logic Testing and Verificationxe2x80x9d, A Ghosh, S. Devadas and R. Newton, Kluwer Academic Publishing, 1992.
[3] xe2x80x9cRuleBase: An Industry-Oriented Formal Verification Toolxe2x80x9d, I. Beer, S. Ben-David, C. Eisner and A. Landver, Design Automation Conference 1996.
[4] xe2x80x9cModel Checking the IBM Gigahertz Processor. An Abstraction Algorithm for High-Performance Netlistsxe2x80x9d by Jason Baymgartner, Tamir Heyman, Adnan Aziz and Vigyan Singhal, Proceedings of the 11th International Conference on Computer-Aided Verification (CAV99), N. Halbwachs and D. Peled (Eds.) Lecture Notes in Computer Science 1633, Springer Verlag, 1999.
[5] xe2x80x9cAlliance Formal Verification Effortxe2x80x9d, S. Mittlemeyar, presentation in the IBM Internal Verification Conference (VAT), September 1998.
[6] xe2x80x9cSymbolic Model Checkingxe2x80x9d, K. McMillan, Kluwer Academic Publishing, 1993.
[7] xe2x80x9cThe Specification of Process Sychronization by Path Expressionxe2x80x9d, R. H. Campbel and A. N. Habermann, in Lecture Notes in Computer Science (G. Goos and J. Heartiness (ed.), Springer, N.Y., 1974, pp. 89-102).
[8] xe2x80x9cPath expressions for complex queries and automatic database program conversionxe2x80x9d. In Proceedings, Very Large Data Bases: 6th international conference, pp. 33-34, IEEE Computer Society, October 1980.
[9] Generalized Path Expression: A High-Level Debugging Mechanismxe2x80x9d, B. Bruegge and P. Hibbard, J. of Systems and Software 3, 1983, pp. 265-276.
[10] xe2x80x9cSwitching and Finite Automata Theoryxe2x80x9d by Zvi Kohavi et al. McGraw Hill College Div.
[11] xe2x80x9cOn-The-Fly Model Checking of RCTL Formulasxe2x80x9d by I. Beer, S. Ben-David and A. Landver, presented in the 1998 Conference on Computer-Aided Verification (CAV98)
The improvements in the silicon, computer and electronic related technologies gave rise to the design of very complicated integrated circuits (ICxe2x80x94referred to also as chips). This trend poses a real challenge to all those automatic and manual verification and inspection procedures which aim at filtering out bugs and faults during the design phase of the specified chips, and thereby to assure with high degree of certainty that faulty chip designs will not be forwarded to manufacture.
Accordingly, the industry is seeking improved technologies, tools and methodologies, to withstand these shortcomings. Thus, it has been suggested to use better techniques for static analysis, e.g. Formal Methods [1]. Such methods have been indeed successfully used in the verification of Finite State Machines (FSMs) in a variety of domains, notably hardware verification [2]. A second, methodological trend, is to ensure that verification starts as early as possible, and is not deferred to later design stages in which detection and correction of flaws is longer and costlier. In fact, an increasing number of design teams are introducing block-level debugging, or exploration, as an integral part of the product development cycle, before integrating the individual units into the target systems [3,4].
The debugging activity is the process in which the implementor explores and experiments with the FSM model by typically testing it against a subset of its feasible inputs. In doing so, the implementor gains insight into the behavior of the FSM model, detects design flaws and corrects them. The related activity of verification (which may or may not be done by the implementor) assures that the implemented FSM meets its functional requirements as thoroughly as possible. In this connection it should be noted that the difference between exploration and verification then, is that inter alia exploration is associated with the implementation process while verification is essentially a post-implementation process. Contemporary exploration methods are limited, as they are generally based on simulation, and require tedious specification of simulation scenarios, which are tested one at a time. That is, all inputs for the model (normally specifying explicitly input vectors) must be specified on a cycle-by-cycle basis to elicit each individual scenario of interest. In practice, given the limitations of contemporary exploration means, and further considering the labor-intensive tedious trial-and-error process, designers tend to carry out exploration of relatively low quality before delivering their FSM models to system verification.1 
1 System verification is the activity in which the individual components designed by separate designers are integrated and tested as a system. 
Furthermore, the specified cycle-by-cycle process typically requires speculation of what input may drive the design towards the behavior of interest. The inherent parallelism of hardware, together with the inadequacy of the simulation platform for this purpose, render hardware exploration low-productivity activity.
The result is that detection of logic errors in the model are deferred to later verification stages where they are costlier to detect and fix, or even overlooked which is obviously undesired.
There is, accordingly, a need in the art to provide for exploration technique. There is a further need in the art to provide for a technique which obviates the specified cycle-by-cycle tedious trial-and-error procedures.
There follows now a glossary of terms, some being conventional and others have been coined herein. The definitions are provided for convenience of explanation only and should by no means be regarded as binding:
The growing realization that exploration of hardware models should be a key component of product design cycle (much like the debugging that is done in software), and the increasing power of Formal Verification engines in recent years, have together laid the ground for the concept of Exploration described therein.
In accordance with one embodiment of the invention, the so called Model Checking tool [6] is exploited for hardware design exploration assuming that the design is represented as a Finite State machine (FSM).
Exploration, as a part of the FSM implementation activity, is the process where the implementor explores some legal paths of the FSM model by testing it with respect to a subset of its legal inputs.
The use of formal methods for hardware exploration provides hardware designers with capabilities that far exceed those offered by contemporary simulators, and furnishes insights into the design behavior. Specifically, using the proposed scheme, designers can specify the type of behavior they wish to explore, rather than specify the input vectors to test this behavior as is done in standard simulation. Also, by using this proposed scheme, designers can reason about sets of scenarios using path specifications, rather than carry out the reasoning one scenario at a time. As a result, the tool of the invention brings about increased productivity which, in turn, results in better, faster development cycles for Finite State Machines.
The proposed technique is not limited to hardware modules and may be applicable to other target modules, such as conventional software modules.
Accordingly, the invention provides for a method of exploring the behavior of a design model, the method comprising the steps of:
a. providing a design model represented as a Finite State Machine (FSM);
b. providing a path specification of interest;
c. exploring the behavior of the design in order to find and present a scenario in the design that meets the path specification.
The invention further provides for a system for exploring the behavior of a design model, the system comprising:
(a) input interface for receiving a design model represented as a Finite State Machine (FSM);
(b) input interface for receiving a path specification of interest;
(c) behavior explorer coupled to at least said input interfaces for exploring the behavior of the design in order to find and present a scenario in the design that meets the path specification.
The invention still further provides for a storage medium that stores data representing a computer implemented program, being capable of
a. receiving a design model represented as a Finite State Machine (FSM);
b. receiving a path specification of interest;
c. exploring the behavior of the design in order to find and present a scenario in the design that meets the path specification.